/*
 * Copyright 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.booleanExpression;

import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.NoSuchElementException;
import java.util.Set;

/**
 * The base abstract class for all Boolean expressions.
 * <br>
 * This class is a very abstract definition of what a Boolean expression is.
 * Such an expression can calculate a truth value given an {@link Assignment}.
 * <br>
 * It implements the Iterable interface and the Iterator must return BooleanExpressions.
 * The idea is that expressions are defined in a recursive way. So all expressions
 * (except for atoms and constants) are constructed given other expressions and the
 * iterator returns them. The {@link Atom} and constant classes ({@link True}, {@link False})
 * return empty iterators.
 * <br>
 * Each expression has an <i>arity</i>. For example the negation has arity 1,
 * disjunction and conjunction have arity 2. (By definition the atoms have arity 1
 * whereas true and false have arity 0).
 * <br>
 * When can also compute the complete size of an expression, that is just the amount
 * of expressions that are used to create the expression (including the expression as well).
 * So atoms and constants have size 1. A conjunction of the form (&phi; &and; &psi;)
 * has the size <i>size(&phi;) + size(&psi;) + 1</i> and so on.
 * <br>
 * Boolean expressions can also be converted to a {@link BooleanFunction}. So the function
 * of a conjunction is a function that accepts two arguments and returns 1 iff. both of
 * the arguments are 1, and so on.
 * <br>
 * If you want to evaluate the truth value of this expression you can of course use the
 * {@link #getTruthValue(Assignment)} method. This is however not recommended because
 * the implementation is in general recursive, and Java gives up very fast. A better
 * way to to so is to use an {@link Evaluator}. 
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public abstract class BooleanExpression implements Iterable<BooleanExpression>
{
	/**
	 * Return the truth value of this expression given an truth assignment.
	 * <br>
	 * So it returns <code>true</code> if &alpha; &#8872; &phi; where &phi; is this formula.
	 * <br>
	 * <b>Note:</b> The implementation of this function is usually a recursive one.
	 * So consider to use an {@link Evaluator}.
	 * 
	 * @param alpha The truth assignment.
	 * 
	 * @return The truth value of this expression given the truth assignment <code>alpha</code>.
	 */
	public abstract boolean getTruthValue(Assignment alpha);
	
	/**
	 * The Boolean function that is defined by this expression.
	 * 
	 * For example the function of a conjunction is a function that accepts two
	 * arguments and returns 1 iff. both of the arguments are 1.
	 * 
	 * @return The Boolean function that is defined by this expression.
	 */
	public abstract BooleanFunction getFunction();
	
	/**
	 * Returns the arity of this expression.
	 * 
	 * For example the negation has arity 1,
	 * disjunction and conjunction have arity 2. (By definition the atoms have arity 1
	 * whereas true and false have arity 0).
	 * 
	 * @return The arity of this expression.
	 */
	public abstract int getArity();
	
	/**
	 * Returns the complete size (amount of all Boolean expression that are used to
	 * create this expression, including this one).
	 * 
	 * For example atoms and constants have size 1. A conjunction of the form 
	 * (&phi; &and; &psi;) has the size <i>size(&phi;) + size(&psi;) + 1</i> and so on.
	 * 
	 * @return The complete size of this expression.
	 */
	public abstract int completeSize();
	
	/**
	 * Returns a set of all variables that occur in the BooleanExpression.
	 * 
	 * Runtime of this Algorithm is linear in the number of subformulae.
	 * 
	 * @return A set containing all variables that occur in this expression.
	 */
	public Set<String> variableSet()
	{
		HashSet<String> result = new HashSet<String>();
		
		LinkedList<BooleanExpression> queue = new LinkedList<BooleanExpression>();
		queue.offer(this);
		while(!queue.isEmpty())
		{
			BooleanExpression next = queue.poll();
			if(next instanceof Atom)
			{
				Atom a = (Atom)next;
				result.add(a.getIdentifier());
			}
			else
			{
				for(BooleanExpression subExp : next)
				{
					queue.offer(subExp);
				}
			}
		}
		
		return result;
	}
}

/**
 * An Iterator that returns two BooleanExpression objects (useful for conjunctin, disjunction etc.).
 * The Iterator prohibits the use of the <code>next</code> method and simply throws an
 * <code>UnsupportedOperationException</code>.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
class TwoElementIterator implements Iterator<BooleanExpression>
{
	/*
	 * The first expression in the sequence.
	 */
	BooleanExpression first;
	/*
	 * The second expession in the sequence.
	 */
	BooleanExpression second;
	/*
	 * A state variable that indicates how many expression have already been returned
	 * by this iterator.
	 */
	short state;
	
	/**
	 * Create a new Iterator.
	 * 
	 * @param first First expression in the sequence.
	 * @param second Second expession in the sequence.
	 */
	public TwoElementIterator(BooleanExpression first, BooleanExpression second)
	{
		this.first = first;
		this.second = second;
		this.state = 0;
	}
	
	@Override
	public boolean hasNext()
	{
		return state < 2;
	}

	@Override
	public BooleanExpression next()
	{
		if(state == 0)
		{
			state++;
			return first;
		}
		if(state == 1)
		{
			state++;
			return second;
		}
		else
		{
			throw new NoSuchElementException("No more elements in subformulae iteration.");
		}
	}

	@Override
	public void remove()
	{
		throw new UnsupportedOperationException("It is not allowed to remove elements from a formula.");
	}
	
}